/**
 * @name bcopy with negative size
 * @description Calling bcopy with a negative size argument will crash the
 *              kernel due to a negative integer overflow.
 * @kind path-problem
 * @problem.severity warning
 * @id apple-xnu/cpp/bcopy-negative-size
 */

import cpp
import semmle.code.cpp.dataflow.TaintTracking
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
import DataFlow::PathGraph

class MyCfg extends TaintTracking::Configuration {
  MyCfg() {
    this = "MyCfg"
  }

  override predicate isSource(DataFlow::Node source) {
    source.asExpr().(FunctionCall).getTarget().getName() = "mbuf_data"
  }

  override predicate isSink(DataFlow::Node sink) {
    exists (FunctionCall call
    | sink.asExpr() = call.getArgument(2) and
      call.getTarget().getName() = "__builtin___memmove_chk" and
      lowerBound(sink.asExpr()) < 0)
  }
}

from DataFlow::PathNode sink, DataFlow::PathNode source, MyCfg cfg
where cfg.hasFlowPath(source, sink)
select sink, source, sink, "The size argument of bcopy might be negative."
